In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements are contained (...) in the type of individuals. Russell's paradox is avoided by placing a type-constraint on lambda-abstraction, rather than by restricting comprehension. (shrink)

We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, predicative (...) logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...) (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

The purpose of this paper is to provide a simple type-free set theory which can be used to give the various readings of collective/distributive sentences.

In this paper, a theory T H based on combining type freeness with logic is introduced and is then used to build a theory of properties which is applied to determiners and quantifiers.

Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...) and the recent revivals of Π-reduction as in [11, 14], illustrate the elegance of giving Π-redexes a status similar to λ-redexes. However, Π-reduction in the λ-cube faces serious problems as shown in [11, 14]: it is not safe as regards subject reduction, it does not satisfy type correctness, it loses the property that the type of an expression is well-formed and it fails to make any expression that contains a Π-redex well-formed. In this paper, we propose a solution to all those problems. The solution is to use a concept that is heavily present in most implementations of programming languages and theorem provers: abbreviations or let-expressions. We will show that the λ-cube extended with Π-conversion and abbreviations satisfies all the desirable properties of the cube and does not face any of the serious problems of Π-reduction. We believe that this extension of the λ-cube is very useful: it gives a full formal study of two concepts that are useful for theorem proving and programming languages. (shrink)

Types were invented by Russell to solve the logical paradoxes that resulted from Frege’s generalisaton of the notion of function. Since, the past 100 years saw new formalisations of the notions of functions and types that extend and put to better use Frege’s and Russell ’s inventions. Most such formalisations are extensions of Church’s simply typed λ-calculus. Currently, types and functions are the heart of logic and computation and not only are they so closely intertwined, but their evolution demands that (...) they be treated in the same manner. Both are usually constructed, abstracted over and instantiated and the operations for abstraction, construction, instantiation and substitution act alike on both. This paper aims to give a framework where the relationship between functions and types takes into account the similarity of their construction, abstraction, instantiation and substitution. For such a “types as functions” framework to work, special forms of function abstraction need to be included. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)

The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: λσ, λse and the suspension calculus. (...) Both λσ and λse when extended with eta-reduction rules, have proved useful for solving higher order unification. We enlarge the suspension calculus with an adequate eta-reduction rule which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta rules of the other two calculi. We prove that λσ and λse as well as λσ and the suspension calculus are non-comparable while λse is more adequate than the suspension calculus in simulating one-step beta-reduction. After defining the eta-reduction rule in the suspension calculus, and after comparing these three calculi of explicit substitutions , we then concentrate on the implementation of the rewrite rules of eta-reduction in these calculi. We note that it is usual practice when implementing the eta rule for substitution calculi, to mix isolated applications of eta-reduction with the application of other rules of the corresponding substitution calculi. The main disadvantage of this practice is that the eta rewrite rules so obtained are unclean because they have an operational semantics different from that of the eta-reduction of the λ-calculus. For the three calculi in question enlarged with adequate eta rules we show how to implement these eta rules. For the λse we build a clean implementation of the eta rule and we prove that it is not possible to follow the same approach for the λσ and λsusp. (shrink)

In this short text, a distinguished philosopher turns his attention to one of the oldest and most fundamental philosophical problems of all: How it is that we are able to sort and classify different things as being of the same natural class? Professor Armstrong carefully sets out six major theories—ancient, modern, and contemporary—and assesses the strengths and weaknesses of each. Recognizing that there are no final victories or defeats in metaphysics, Armstrong nonetheless defends a traditional account of universals as the (...) most satisfactory theory we have.This study is written for advanced students, but as Armstrong goes considerably beyond his earlier work on this topic, it will interest professional scholars as well. Carefully plotted and clearly written, Universals is both a paradigm of exposition and a case study on the value of careful analysis of fundamental issues in philosophy. (shrink)

In this important study D. M. Armstrong offers a comprehensive system of analytical metaphysics that synthesises but also develops his thinking over the last twenty years. Armstrong's analysis, which acknowledges the 'logical atomism' of Russell and Wittgenstein, makes facts the fundamental constituents of the world, examining properties, relations, numbers, classes, possibility and necessity, dispositions, causes and laws. All these, it is argued, find their place and can be understood inside a scheme of states of affairs. This is a comprehensive and (...) rigorously this-worldly account of the most general features of reality, argued from a distinctive philosophical perspective, and it will appeal to a wide readership in analytical philosophy. (shrink)

This chapter explores the debate between contemporary projectivists or expressivists, and the advocates of sensibility theory. Both positions are best viewed as forms of sentimentalism — the theory that evaluative concepts must be explicated by appeal to the sentiments. It argues that the sophisticated interpretation of such notions as “true” and “objective” that are offered by defenders of these competing views ultimately undermines the significance of their meta-ethical disputes over “cognitivism” and “realism” about value. Their fundamental disagreement lies in moral (...) psychology; it concerns how best to understand the emotions to which sentimentalist theories must appeal. (shrink)

A substantial guide providing an overview of both physicalism and metaphysical naturalism, reviewing both questions of formulation and justification for both doctrines. Includes a diagnostic strategy for understanding talk of naturalism as a metaphysical thesis.

Inside What Would Plato Do?, you'll find the basics of philosophy, written in an easy, digestible way we can all understand, along with questions to help you apply these important theories to your own life. So, after you've learned about a philosophical concept, you'll then be challenged to test yourself and see how the results can impact your daily life. For instance, after learning about Kant's theory of morality and the importance of intention you're challenged with questions like: Can good (...) people do bad things? Was there a time when you intended to do something helpful that ended up being hurtful? Does that make you a good person (because you intended to do good) or a bad person (because the results were bad)? What Would Plato Do? will not only help you better understand some of the greatest thinkers ever but will also help you think of the world around you in a whole new way! (shrink)

This paper is a review of the influence that lógos has had on ancient Greek, Jewish, and Christian writings. During the philosophical era known as Middle Platonism, the concept/ontology of the lógos played a unique role in enabling Pagan, Jewish, and Christian intellectuals to communicate on a small space of common ground.

We are immersed within an odorous sea of chemical currents that we parse into individual odors with complex structures. Odors have been posited as determined by the structural relation between the molecules that compose the chemical compounds and their interactions with the receptor site. But, naturally occurring smells are parsed from gaseous odor plumes. To give a comprehensive account of the nature of odors the chemosciences must account for these large distributed entities as well. We offer a focused review of (...) what is known about the perception of odor plumes for olfactory navigation and tracking, which we then connect to what is known about the role odorants play as properties of the plume in determining odor identity with respect to odor quality. We end by motivating our central claim that more research needs to be conducted on the role that odorants play within the odor plume in determining odor identity. (shrink)

The central insight of Darwin's Origin of Species is that evolution is an ecological phenomenon, arising from the activities of organisms in the 'struggle for life'. By contrast, the Modern Synthesis theory of evolution, which rose to prominence in the twentieth century, presents evolution as a fundamentally molecular phenomenon, occurring in populations of sub-organismal entities - genes. After nearly a century of success, the Modern Synthesis theory is now being challenged by empirical advances in the study of organismal development and (...) inheritance. In this important study, D. M. Walsh shows that the principal defect of the Modern Synthesis resides in its rejection of Darwin's organismal perspective, and argues for 'situated Darwinism': an alternative, organism-centred conception of evolution that prioritises organisms as adaptive agents. His book will be of interest to scholars and advanced students of evolutionary biology and the philosophy of biology. (shrink)

We perceive smells as perduring complex entities within a distal array that might be conceived of as smellscapes. However, the philosophical orthodoxy of Odor Theories has been to deny that smells are perceived as having a distal location. Recent challenges have been mounted to Odor Theories’ veracity in handling the timescale of olfactory perception, how it individuates odors as a distal entities, and their claim that olfactory perception is not spatial. The paper does not aim to dispute these criticisms. Rather, (...) what will be shown is that Molecular Structure Theory, a refinement of Odor Theory, can be further developed to handle these challenges. The theory is further refined by focusing on distal perception that requires considering the perceptual object as mereologically complex persisting odor against a background scene conceived of as a smellscape. What will be offered is an expansion of Molecular Structure Theory to account for distal smell perception within natural environments. (shrink)

This is a book grounded in the real ethical challenges of modern business practice, with a world-religious perspective so necessary in an era of globalization.

John Foster’s book, The Nature of Perception, is written to defend his Idealist, or Berkeleyan, theory of perception. One view that he is concerned to reject is what he usefully calls the ‘Cognitivist’ theory of perception. I am named as one of its defenders. His critique of the theory serves me as a good starting point and as a stimulus for a new defense of the theory.

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:Transcendental Phenomenology as Human Possibility: Husserl and Fink on the Phenomenologizing Subject by Denis DŽANIĆD. J. HobbsDŽANIĆ, Denis. Transcendental Phenomenology as Human Possibility: Husserl and Fink on the Phenomenologizing Subject. Cham: Springer, 2023. x + 236 pp. Cloth, $119.99Denis Džanić’s Transcendental Phenomenology as Human Possibility, despite its superficially historical focus on a specific period of collaboration between Edmund Husserl and his somewhat wayward protégé Eugen Fink, addresses key (...) systematic issues in transcendental phenomenology, namely, how the act of phenomenologizing should be understood in connection with the specific human beings who aim to become phenomenologists, and what the answer to this question tells us about both the genuine subject of phenomenology and the motivation for phenomenologizing. These questions are important for our understanding of not only the historical development of phenomenology but also the practice and goals of phenomenology—specifically, for a conception of phenomenologizing as a project in which we, as particular, historical, empirical figures, might want to engage.Much of the book focuses on laying the groundwork for understanding these complicated issues both historically and systematically. Džanić does an admirable job of tracing the rapidly evolving interactions between Husserl and Fink, both as intellectual collaborators on this philosophical project and as a pair of very human figures who ultimately found themselves pursuing quite different solutions to the problems of the subject and origin of phenomenology. He focuses particularly on the Sixth Cartesian Meditation, Fink’s attempt to extend Husserl’s famous text to include a phenomenology of the act of phenomenologizing itself (including Husserl’s marginal comments on the text), although he draws on a number of other significant texts and manuscripts (mostly Husserl’s, albeit with an extended aside on Heidegger) wherever they are helpful for explicating the complex evolution of Husserl’s thought on the subject. Admittedly, the book thus takes on a challenging task—both because of the difficult nature of this topic and because of the obscurity of the technical terms required to discuss it. However, despite the necessarily enigmatic character of the relevant language, Džanić’s attempts to explore the main outlines of this issue are worthwhile, particularly due to his ability to resist the temptation to view Husserl’s thought here as monolithic.In the early chapters, Džanić explicates in detail the rather complicated solution that Fink proposed to this difficulty, namely, the abandonment (to some extent) of the ultimately human origin of phenomenology in favor of a fundamentally nonhuman (and eventually meontic) conception of the transcendental ego, which generated a great deal of elaborate and (at least in the Sixth Meditation) inadequately supported speculation. For Fink, both the motivation to phenomenologize and the act of phenomenologizing itself ultimately stem from a source that is fundamentally prior to—in a(n onto)logical rather than temporal sense—any empirical ego or empirical act of phenomenologizing, a source that merely “enworlds” itself (in various complicated senses that Džanić does [End Page 145] an admirable job of clarifying) in the apparently anthropologistic, everyday world of individual phenomenologists. Džanić calls this interpretation of phenomenology Fink’s “epistemological anti-humanism,” and it serves as the basis for one potential (radically anti-Heideggerian but nevertheless somewhat disappointing) solution to the question of why we should phenomenologize at all. As Džanić notes, this solution was at least briefly taken up by Fink’s mentor Husserl himself, although the degree to which Husserl actually endorsed this path beyond the level of a fleeting flirtation remains questionable. Ultimately, as Džanić rightly highlights and as becomes abundantly clear in Husserl’s (often rather scathing) notes on Fink’s Sixth Cartesian Meditation, he abandoned this interpretation.Accordingly, in the later chapters of the book, Džanić traces Husserl’s ultimate development of a quite different solution to the problems of the origin and motivation of phenomenology—a solution that, unlike his brief foray into Finkian grandeur, views the act of phenomenologizing as essentially rooted in human possibility (that is, as part of the famous lifeworld that features so prominently in Husserl’s work, especially in the Crisis and other late texts). After his collaboration with and... (shrink)

The aim of the present study was to assess the impact of past traumatic war experiences on preadolescents in the Gaza Strip, which could be useful for psychological intervention with current and future child victims. Participants were 521 preadolescents from United Nations Relief and Works Agency for Palestine Refugees in the Near East (UNRWA) schools, aged 11 and 13 years old. Sections I to IV from Iraqi Version-Arabic of Harvard Trauma Questionnaire was used to assess trauma experiences and Post-Traumatic Stress (...) Disorder (PTSD). The results show that the preadolescents in the Gaza Strip witnessed the destruction of their homes and the murder of family members and friends. A quarter of the individuals assessed either suffered torture or witnessed others undergoing it, including sexual assaults. Almost half of them experienced a lack of food and clean water. The traumatic and torture experiences seriously affected preadolescents’ mental health as 26.29% met criteria for the diagnosis of PTSD. The data analysis revealed two PTSD modalities, with the severity of impact depending on whether social implications were involved. Further research is required to check whether these two modalities fit to PTSD and complex PTSD. Understanding the effects of past wars on preadolescents in Gaza and distinguishing between different PTSD types could enhance comprehension of the impacts of current attacks on child victims. It can also aid in determining the type of intervention needed to minimize the impact on the mental health of Palestinian youth, enhancing their resilience through psychological and social support. (shrink)

This article seeks to present Vygotsky's theoretical perspective as an integral whole as an antidote to the desire to plunder his work for isolated insights. The first part of the paper treats Vygotsky's views on method: his critique of the prevailing psychological orthodoxies; his recommendation that the higher mental functions be seen as standing in interfunctional relations of mutual determination; his technique of 'unit analysis'. The second part discusses the method in action: Vygotsky's genetic account of the development of consciousness, (...) on which the key point in ontogenesis is taken to be the convergence of two intitially independently developing faculties: thought and speech; the notion of internalisation and its defence; the critique of Piaget; the concept of 'inner speech' and developed thought. The author hopes this article will serve as an aid to reading the limited sources of Vygotsky's writings presently available in English. (shrink)

In his 1922/1923 articles for the Japanese magazine _Kaizō_, Edmund Husserl identifies a particular “humanity” or human culture by the purposeful idea [_Zweckidee_] consciously embraced by the community. This purposeful idea is attained through rational self-formation on the part of the community in a manner analogous to the rational self-formation of the individual human being. Thereafter, it can be referenced to distinguish different cultures (or stages of cultural development) from one another through its objective manifestation in communal groups and cultural (...) products, as Husserl retraces in a historical account of the development of Western history. This paper explores the essential character of this conception of the purposeful idea from both an exegetical and a systematic perspective, examining in particular the relationship between such an idea and the values experienced by individual subjects within a culture (which are, according to Husserl, also available at the level of objective culture in relation to a communal subject). The paper argues that Husserl’s basic conception of the purposeful idea is a good model for understanding certain essential characteristics of cultural constitution in general, although some of his fundamental assumptions—especially the strict identity he attempts to establish between a purposeful idea as such and the specific goal of universal, rational self-understanding—turn out to be somewhat more questionable in light of the connection between the purposeful idea and the genuinely felt values underlying it. (shrink)

ABSTRACTOne long-running conundrum in Husserlian phenomenology revolves around the question of the identity of what Husserl calls the transcendental ego, a mysterious figure that he identifies as the subject of a genuinely transcendental phenomenology. In dialogue with both Husserl and his assistant and collaborator Eugen Fink, I attempt in this article to give a solid account of the identity of this transcendental ego, and in particular to explain the connection between this figure and the empirical ego of the individual phenomenologist. (...) I make particular reference to Fink's depiction of a "personal union" between these two egos in his Sixth Cartesian Meditation and to certain unclear hints in Husserl's 1923/1924 lectures on First Philosophy. Ultimately, I develop my own account of such a union, which explains the transcendental ego as a certain mode in which the phenomenologist might investigate his own experiences. On this basis, I argue, the status of phenomenology as a transcendental discipline can be understood without subjecting that discipline to certain criticisms that have been levelled against it. (shrink)

Reflection Principles are commonly thought to produce only strong axioms of infinity consistent with V = L. It would be desirable to have some notion of strong reflection to remedy this, and we have proposed Global Reflection Principles based on a somewhat Cantorian view of the universe. Such principles justify the kind of cardinals needed for, inter alia , Woodin’s Ω-Logic.

When it originated in the late 19th century, psychometrics was a field with both a scientific and a social mission: psychometrics provided new methods for research into individual differences, and at the same time, these psychometric instruments were considered a means to create a new social order. In contrast, contemporary psychometrics - due to its highly technical nature and its limited involvement in substantive psychological research - has created the impression of being a value-free discipline. In this article, we develop (...) a contrasting characterization of contemporary psychometrics as a value-laden discipline. We expose four such values: that individual differences are quantitative (rather than qualitative), that measurement should be objective in a specific sense, that test items should be fair, and that utility of a model is more important than its truth. Our goal is not to criticize psychometrics for employing these values, but rather to bring them into the open and to show that these values are not inevitable and are in need of systematic evaluation. (shrink)

We present the system SUBSEXPL used for simulating and comparing explicit substitutions calculi. The system allows the manipulation of expressions of the λ-calculus and of three different styles of explicit substitutions: the λσ, the λse and the suspension calculus. A variation of the suspension calculus, which allows for combination of steps of β-contraction is included too. Implementations of the η-reduction are provided for each style. Other explicit substitutions calculi can be easily incorporated into the system due to its modular structure. (...) The uses of the system include: the visualization of the contractions of the λ-calculus in de Bruijn notation, and of guided one-step reductions as well as normalization via each of the associated substitution calculi. Many useful facilities are included: reductions can be easily recorded as text files, LATEX outputs can be generated and several examples for dealing with arithmetic operations and computational operators such as conditionals and repetitions in the λ-calculus are available. The system can be executed over Emacs using the x-symbol mode in such a way that λ-terms and terms of the explicit substitutions calculi are represented in its natural syntax avoiding the necessity of repeatedly generating LATEX outputs. The system has been of great help for systematically comparing explicit substitutions calculi, as well as for understanding properties of explicit substitutions such as the Preservation of Strong Normalization. In addition, it has been used for teaching basic properties of the λ-calculus such as: computational adequacy, the usefulness of de Bruijn's notation and of making explicit substitutions in real implementations. (shrink)

According to historical theories of biological function, a trait's function is determined by natural selection in the past. I argue that, in addition to historical functions, ahistorical functions ought to be recognized. I propose a theory of biological function which accommodates both. The function of a trait is the way it contributes to fitness and fitness can only be determined relative to a selective regime. Therefore, the function of a trait can only be specified relative to a selective regime. Apart (...) from its desirable pluralism, only this view of relational function can support the function/accident and function/malfunction distinctions commonly thought to be part of the concept of function. Furthermore, only relational function correctly characterizes the explanatory consequences of function attributions in evolutionary biology. (shrink)